Termination w.r.t. Q proof of /tmp/tmp4QAFnV/2.42.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

flatten(nil) → nil
flatten(unit(x)) → flatten(x)
flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(x, nil) → x
++(nil, y) → y
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

flatten(nil) → nil
flatten(unit(x)) → flatten(x)
flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(x, nil) → x
++(nil, y) → y
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

flatten(nil) → nil
flatten(unit(x)) → flatten(x)
flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(x, nil) → x
++(nil, y) → y
++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

flatten(nil) → nil
flatten(unit(x)) → flatten(x)
flatten(++(x, y)) → ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) → ++(flatten(x), flatten(y))
flatten(flatten(x)) → flatten(x)
rev(nil) → nil
rev(unit(x)) → unit(x)
rev(++(x, y)) → ++(rev(y), rev(x))
rev(rev(x)) → x
++(x, nil) → x
++(nil, y) → y

Used ordering:
Polynomial interpretation [25]:

POL(++(x₁, x₂)) = 2 + x₁ + x₂
POL(flatten(x₁)) = 1 + 2·x₁
POL(nil) = 0
POL(rev(x₁)) = 1 + 2·x₁
POL(unit(x₁)) = 1 + 2·x₁

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

++(++(x, y), z) → ++(x, ++(y, z))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

++(++(x, y), z) → ++(x, ++(y, z))

Used ordering:
Polynomial interpretation [25]:

POL(++(x₁, x₂)) = 2 + 2·x₁ + x₂

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RisEmptyProof

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.